$\forall$${\it the\_es}$:event\_system\{i:l\}, $e$,${\it e'}$,$y$:es{-}E(${\it the\_es}$).
\\[0ex]l\_before(${\it e'}$; $y$; before($e$); es{-}E(${\it the\_es}$)) $\Rightarrow$ es{-}locl(${\it the\_es}$; ${\it e'}$; $y$)